local{-}state($f$;${\it base}$;$X$;$e$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if $e$ $\in_{b}$ $X$ then $f$(prior{-}state($f$;${\it base}$;$X$;$e$),$X$($e$)) else prior{-}state($f$;${\it base}$;$X$;$e$) fi